FDL - Nuprl Lemma : es-trigger-loc

Nuprl Lemma : es-trigger-loc

es:ES, A, V:Type, i:Id, knd:Knd, ds:x:Id fp

Type, f:(State(ds)

V

(A + Top)).
(

e:E. (loc(e) = i)

(kind(e) = knd)

((valtype(e)

r V) & (state@loc(e)

r State(ds))))

(

e:E. (

(e

es-trigger(es;i;knd;ds;f)))

(loc(e) = i))

Definitions left + right, P Q, Dec(P), x:A. B(x), loc(e), <a, b>, Id, s = t, b, P Q, E, Knd, valtype(e), state@i, State(ds), x:A B(x), P & Q, x:AB(x), Top, Type, a:A fp B(a), ES, ff, es-trigger(es;i;knd;ds;f), e X, s ~ t, t T, Void, x:A.B(x), False

Lemmas es-trigger-not-loc, decidable equal Id